(VERS1 0 (NIL ((LINENAME SORTINFO (LN& #& . 0) (LN& #& . 22) (LN& #& . 35) (LN& #& . 36) (LN& #& . 40) (LN& #& . 41) (LN& #& . 42) (LN& #& . 46) (LN& #& . 54)) (LINENAME SIMPINFO (LN& #& . 22) (LN& #& . 58) (LN& #& . 66) (LN& #& . 67) (LN& #& . 68) (LN& #& . 74) (LN& #& . 75) (LN& #& . 76) (LN& #& . 77) (LN& #& . 78) (LN& #& . 79) (LN& #& . 80) (LN& #& . 81) (LN& #& . 46)) (LINENAME NILPROP (LN& #& . 82) (LN& #& . 83) (LN& #& . 84) (LN& #& . 58)) (LINENAME CONSFACTS (LN& #& . 66) (LN& #& . 67) (LN& #& . 75) (LN& #& . 76)) (LINENAME LISTINDUCTION (LN& #& . 85)) (LINENAME SEXPINDUCTION (LN& #& . 88)) (LINENAME LISTAPPEND (LN& #& . 42)) (LINENAME DEFINFO (LN& #& . 89) (LN& #& . 90) (LN& #& . 93) (LN& #& . 96) (LN& #& . 97) (LN& #& . 100) (LN& #& . 110) (LN& #& . 111)) (LINENAME APPENDFACTS (LN& #& . 80) (LN& #& . 81)) (LINENAME REVERSEAPPEND (LN& #& . 114)) (LINENAME REVERSEREVERSE (LN& #& . 115))) (MATCH (#& . 102) (#& . 105) (#& . 109) (#& . 100) (#& . 116) (#& . 110) (#& . 117) (#& . 113) (#& . 111) (#& . 118) (#& . 119) (#& . 120)) (LISPAX (#& . 2) (#& . 30) (#& . 121) (#& . 87) (#& . 65) (#& . 125) (#& . 27) (#& . 70) (#& . 60) (#& . 24) (#& . 20) (#& . 0) (#& . 127) (#& . 22) (#& . 128) (#& . 82) (#& . 129) (#& . 83) (#& . 130) (#& . 84) (#& . 131) (#& . 58) (#& . 132) (#& . 35) (#& . 133) (#& . 66) (#& . 134) (#& . 67) (#& . 135) (#& . 68) (#& . 136) (#& . 74) (#& . 137) (#& . 75) (#& . 138) (#& . 76) (#& . 139) (#& . 85) (#& . 140) (#& . 88) (#& . 141) (#& . 38) (#& . 36) (#& . 142) (#& . 77) (#& . 143) (#& . 40) (#& . 144) (#& . 78) (#& . 145) (#& . 41) (#& . 146) (#& . 79) (#& . 147) (#& . 44) (#& . 42) (#& . 148) (#& . 89) (#& . 149) (#& . 80) (#& . 150) (#& . 81) (#& . 151) (#& . 48) (#& . 46) (#& . 152) (#& . 153) (#& . 92) (#& . 90) (#& . 154) (#& . 95) (#& . 93) (#& . 155) (#& . 56) (#& . 54) (#& . 156) (#& . 96) (#& . 157) (#& . 114) (#& . 158) (#& . 115) (#& . 159) (#& . 99) (#& . 97) (#& . 160))) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 85 .) (NIL . (COMMENTL LNAME REVERSEREVERSE) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 82 .) (NIL . (COMMENTL LNAME REVERSEAPPEND) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 80 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 78 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 76 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 73 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 70 .) ((((∀ ALIST)) (⊃ (¬ (NULL ALIST)) (∧ (¬ (ATOM (CAR ALIST))) (ATOM (CAR (CAR ALIST)))))) . (AXIOM (TM& ((∀ ALIST)) (⊃ (¬ (NULL ALIST)) (∧ (¬ (ATOM (CAR ALIST))) (ATOM (CAR (CAR ALIST))))))) . NIL . ((ALIST #& . 47) (CAR #& . 69) (ATOM #& . 61) (NULL #& . 59)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 67 .) (NIL . (COMMENTL LNAME SIMPINFO SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 66 .) (NIL . (COMMENTL LNAME APPENDFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 63 .) (NIL . (COMMENTL LNAME APPENDFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 61 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 59 .) (NIL . (COMMENTL LNAME SORTINFO LISTAPPEND) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 57 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 54 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 52 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 50 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 48 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 46 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 44 .) (NIL . (COMMENTL LNAME SEXPINDUCTION) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 41 .) (NIL . (COMMENTL LNAME LISTINDUCTION) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 39 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 37 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 35 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 33 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 31 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 29 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 27 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 25 .) (NIL . (COMMENTL LNAME SIMPINFO NILPROP) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 23 .) (NIL . (COMMENTL LNAME NILPROP) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 21 .) (NIL . (COMMENTL LNAME NILPROP) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 19 .) (NIL . (COMMENTL LNAME NILPROP) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 17 .) (NIL . (COMMENTL LNAME SORTINFO SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 15 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 13 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 125) . CONS .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS #& . 126)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 6 .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 121) . B .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 121) . A .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 121) . C .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((C #& . 122) (A #& . 123) (B #& . 124)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 3 .) ((¬ (= (MATCH PAT EXP ALIST) NO)) . (ASSUME (TM& ¬ (= (MATCH PAT EXP ALIST) NO))) . NIL . ((MATCH #& . 108) (NO #& . 104) (EXP #& . 103) (PAT #& . 101) (ALIST #& . 47)) . NIL . NIL . ((&& . 1)) . NIL . MATCH . NIL . NIL . 12 .) ((⊃ (∧ (((∀ X)) (⊃ (ATOM X) (((∀ EXP ALIST)) (⊃ (¬ (= (MATCH X EXP ALIST) NO)) (= (SUBLISQ X (MATCH X EXP ALIST)) EXP))))) (((∀ X Y)) (⊃ (∧ (((∀ EXP ALIST)) (⊃ (¬ (= (MATCH X EXP ALIST) NO)) (= (SUBLISQ X (MATCH X EXP ALIST)) EXP))) (((∀ EXP ALIST)) (⊃ (¬ (= (MATCH Y EXP ALIST) NO)) (= (SUBLISQ Y (MATCH Y EXP ALIST)) EXP)))) (((∀ EXP ALIST)) (⊃ (¬ (= (MATCH (~ X Y) EXP ALIST) NO)) (= (SUBLISQ (~ X Y) (MATCH (~ X Y) EXP ALIST)) EXP)))))) (((∀ X EXP ALIST)) (⊃ (¬ (= (MATCH X EXP ALIST) NO)) (= (SUBLISQ X (MATCH X EXP ALIST)) EXP)))) . (∀E PHI (TM& ((λ PAT)) (((∀ EXP ALIST)) (⊃ (¬ (= (MATCH PAT EXP ALIST) NO)) (= (SUBLISQ PAT (MATCH PAT EXP ALIST)) EXP)))) (LN& #& . 88) (MODE& STANDARD)) . NIL . ((Y #& . 34) (X #& . 29) (~ #& . 26) (ATOM #& . 61) (SUBLISQ #& . 112) (MATCH #& . 108) (NO #& . 104) (EXP #& . 103) (ALIST #& . 47)) . NIL . NIL . ((#& . 88)) . NIL . MATCH . NIL . NIL . 11 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . MATCH . NIL . NIL . 10 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . MATCH . NIL . NIL . 7 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . MATCH . NIL . NIL . 5 .) ((((∀ U)) (= (REVERSE (REVERSE U)) U)) . (AXIOM (TM& ((∀ U)) (= (REVERSE (REVERSE U)) U))) . NIL . ((REVERSE #& . 55) (U #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 81 .) ((((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U)))) . (AXIOM (TM& ((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U))))) . NIL . ((V #& . 14) (U #& . 1) (REVERSE #& . 55)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 79 .) (NIL . (DECL (SUBLISQ) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((SUBLISQ #& . 112)) . NIL . NIL . NIL . NIL . MATCH . NIL . NIL . 8 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 113) . SUBLISQ .) ((((∀ PAT ALIST)) (= (SUBLISQ PAT ALIST) (CONDI (ATOM PAT) ((((λ U)) (CONDI (NULL U) LOSE (CDR U))) (ASSOC PAT ALIST)) (CONDI (= (CAR PAT) QUOTE) (CAR (CDR PAT)) (~ (SUBLISQ (CAR PAT) ALIST) (SUBLISQ (CDR PAT) ALIST)))))) . (AXIOM (TM& ((∀ PAT ALIST)) (= (SUBLISQ PAT ALIST) (CONDI (ATOM PAT) ((((λ U)) (CONDI (NULL U) LOSE (CDR U))) (ASSOC PAT ALIST)) (CONDI (= (CAR PAT) QUOTE) (CAR (CDR PAT)) (~ (SUBLISQ (CAR PAT) ALIST) (SUBLISQ (CDR PAT) ALIST))))))) . NIL . ((ATOM #& . 61) (CDR #& . 71) (CAR #& . 69) (~ #& . 26) (ALIST #& . 47) (ASSOC #& . 91) (NULL #& . 59) (U #& . 1) (PAT #& . 101) (QUOTE #& . 107) (LOSE #& . 106) (SUBLISQ #& . 112)) . NIL . NIL . ((&& . 1)) . NIL . MATCH . NIL . NIL . 9 .) ((((∀ PAT EXP ALIST)) (= (MATCH PAT EXP ALIST) (CONDI (ATOM PAT) ((((λ A1)) (CONDI (NULL A1) (~ (~ PAT EXP) ALIST) (CONDI (= (CDR (CAR A1)) EXP) ALIST NO))) (ASSOC PAT ALIST)) (CONDI (= (CAR PAT) QUOTE) (CONDI (= (CAR (CDR PAT)) EXP) ALIST NO) (CONDI (ATOM EXP) NO (MATCH (CAR PAT) (CAR EXP) (MATCH (CDR PAT) (CDR EXP) ALIST))))))) . (AXIOM (TM& ((∀ PAT EXP ALIST)) (= (MATCH PAT EXP ALIST) (CONDI (ATOM PAT) ((((λ A1)) (CONDI (NULL A1) (~ (~ PAT EXP) ALIST) (CONDI (= (CDR (CAR A1)) EXP) ALIST NO))) (ASSOC PAT ALIST)) (CONDI (= (CAR PAT) QUOTE) (CONDI (= (CAR (CDR PAT)) EXP) ALIST NO) (CONDI (ATOM EXP) NO (MATCH (CAR PAT) (CAR EXP) (MATCH (CDR PAT) (CDR EXP) ALIST)))))))) . NIL . ((MATCH #& . 108) (NO #& . 104) (QUOTE #& . 107) (EXP #& . 103) (PAT #& . 101) (NULL #& . 59) (ASSOC #& . 91) (ALIST #& . 47) (A1 #& . 53) (~ #& . 26) (CAR #& . 69) (CDR #& . 71) (ATOM #& . 61)) . NIL . NIL . ((&& . 1)) . NIL . MATCH . NIL . NIL . 6 .) (NIL . (DECL (MATCH) (OT& (GROUND GROUND GROUND) . GROUND) CONSTANT) . NIL . ((MATCH #& . 108)) . NIL . NIL . NIL . NIL . MATCH . NIL . NIL . 3 .) (CONSTANT . ((GROUND GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 109) . MATCH .) (CONSTANT . GROUND . SEXP . NIL . NIL . (#& . 105) . QUOTE .) (CONSTANT . GROUND . SEXP . NIL . NIL . (#& . 105) . LOSE .) (NIL . (DECL (NO QUOTE LOSE) (OT& . GROUND) CONSTANT SEXP) . NIL . ((LOSE #& . 106) (NO #& . 104) (SEXP #& . 19) (QUOTE #& . 107)) . NIL . NIL . NIL . NIL . MATCH . NIL . NIL . 2 .) (CONSTANT . GROUND . SEXP . NIL . NIL . (#& . 105) . NO .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 102) . EXP .) (NIL . (DECL (PAT EXP) (OT& . GROUND)) . NIL . ((EXP #& . 103) (PAT #& . 101)) . NIL . NIL . NIL . NIL . MATCH . NIL . NIL . 1 .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 102) . PAT .) ((((∀ PAT EXP)) (= (MATCH PAT EXP NO) NO)) . (AXIOM (TM& ((∀ PAT EXP)) (= (MATCH PAT EXP NO) NO))) . NIL . ((PAT #& . 101) (EXP #& . 103) (NO #& . 104) (MATCH #& . 108)) . NIL . NIL . ((&& . 1)) . NIL . MATCH . NIL . NIL . 4 .) (NIL . (DECL (SUBST) (OT& (GROUND GROUND GROUND) . GROUND) CONSTANT) . NIL . ((SUBST #& . 98)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 83 .) (CONSTANT . ((GROUND GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 99) . SUBST .) ((((∀ X Y Z)) (= (SUBST X Y Z) (CONDI (ATOM Z) (CONDI (= Z Y) X Z) (~ (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z)))))) . (AXIOM (TM& ((∀ X Y Z)) (= (SUBST X Y Z) (CONDI (ATOM Z) (CONDI (= Z Y) X Z) (~ (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))) . NIL . ((Y #& . 34) (X #& . 29) (Z #& . 31) (~ #& . 26) (CAR #& . 69) (CDR #& . 71) (ATOM #& . 61) (SUBST #& . 98)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 84 .) ((((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U)))))) . (AXIOM (TM& ((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U))))))) . NIL . ((REVERSE #& . 55) (NULL #& . 59) (CDR #& . 71) (CAR #& . 69) (NNIL #& . 64) (U #& . 1)) . ((* #& . 43) (LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 77 .) (NIL . (DECL (MEMBER) (OT& (GROUND GROUND) . TRUTHVAL) CONSTANT) . NIL . ((MEMBER #& . 94)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 71 .) (CONSTANT . ((GROUND GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . (#& . 95) . MEMBER .) ((((∀ X U)) (≡ (MEMBER X U) (∧ (¬ (NULL U)) (∨ (= X (CAR U)) (MEMBER X (CDR U)))))) . (AXIOM (TM& ((∀ X U)) (≡ (MEMBER X U) (∧ (¬ (NULL U)) (∨ (= X (CAR U)) (MEMBER X (CDR U))))))) . NIL . ((NULL #& . 59) (CDR #& . 71) (CAR #& . 69) (X #& . 29) (U #& . 1) (MEMBER #& . 94)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 72 .) (NIL . (DECL (ASSOC) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((ASSOC #& . 91)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 68 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 92) . ASSOC .) ((((∀ X ALIST)) (= (ASSOC X ALIST) (CONDI (NULL ALIST) NNIL (CONDI (= X (CAR (CAR ALIST))) (CAR ALIST) (ASSOC X (CDR ALIST)))))) . (AXIOM (TM& ((∀ X ALIST)) (= (ASSOC X ALIST) (CONDI (NULL ALIST) NNIL (CONDI (= X (CAR (CAR ALIST))) (CAR ALIST) (ASSOC X (CDR ALIST))))))) . NIL . ((ALIST #& . 47) (X #& . 29) (NNIL #& . 64) (CAR #& . 69) (CDR #& . 71) (NULL #& . 59) (ASSOC #& . 91)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 69 .) ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (~ (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (~ (CAR U) (* (CDR U) V)))))) . NIL . ((V #& . 14) (U #& . 1) (~ #& . 26) (CAR #& . 69) (CDR #& . 71) (NULL #& . 59)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 58 .) ((((∀ PHI)) (⊃ (∧ (((∀ X)) (⊃ (ATOM X) (PHI X))) (((∀ X Y)) (⊃ (∧ (PHI X) (PHI Y)) (PHI (~ X Y))))) (((∀ X)) (PHI X)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (((∀ X)) (⊃ (ATOM X) (PHI X))) (((∀ X Y)) (⊃ (∧ (PHI X) (PHI Y)) (PHI (~ X Y))))) (((∀ X)) (PHI X))))) . NIL . ((Y #& . 34) (X #& . 29) (PHI #& . 86) (~ #& . 26) (ATOM #& . 61)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 40 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI #& . 86)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 4 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . (#& . 87) . PHI .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (~ X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (~ X U))))) (((∀ U)) (PHI U))))) . NIL . ((~ #& . 26) (NNIL #& . 64) (PHI #& . 86) (X #& . 29) (U #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 38 .) ((((∀ U)) (⊃ (ATOM U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (⊃ (ATOM U) (= U NNIL)))) . NIL . ((U #& . 1) (NNIL #& . 64) (ATOM #& . 61)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 20 .) ((ATOM NNIL) . (AXIOM (TM& ATOM NNIL)) . NIL . ((ATOM #& . 61) (NNIL #& . 64)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 18 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((U #& . 1) (NNIL #& . 64) (NULL #& . 59)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 16 .) ((((∀ X U V)) (= (* (~ X U) V) (~ X (* U V)))) . (AXIOM (TM& ((∀ X U V)) (= (* (~ X U) V) (~ X (* U V))))) . NIL . ((V #& . 14) (U #& . 1) (X #& . 29) (~ #& . 26)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 62 .) ((((∀ U)) (= (* NNIL U) U)) . (AXIOM (TM& ((∀ U)) (= (* NNIL U) U))) . NIL . ((NNIL #& . 64) (U #& . 1)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 60 .) ((((∀ X Y Z)) (= (LIST X Y Z) (~ X (LIST Y Z)))) . (AXIOM (TM& ((∀ X Y Z)) (= (LIST X Y Z) (~ X (LIST Y Z))))) . NIL . ((Y #& . 34) (X #& . 29) (Z #& . 31) (~ #& . 26)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 53 .) ((((∀ X Y)) (= (LIST X Y) (~ X (LIST Y)))) . (AXIOM (TM& ((∀ X Y)) (= (LIST X Y) (~ X (LIST Y))))) . NIL . ((Y #& . 34) (X #& . 29) (~ #& . 26)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 49 .) ((((∀ X)) (= (LIST X) (~ X NNIL))) . (AXIOM (TM& ((∀ X)) (= (LIST X) (~ X NNIL)))) . NIL . ((X #& . 29) (NNIL #& . 64) (~ #& . 26)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 45 .) ((((∀ X Y)) (= (CDR (~ X Y)) Y)) . (AXIOM (TM& ((∀ X Y)) (= (CDR (~ X Y)) Y))) . NIL . ((Y #& . 34) (X #& . 29) (~ #& . 26) (CDR #& . 71)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 36 .) ((((∀ X Y)) (= (CAR (~ X Y)) X)) . (AXIOM (TM& ((∀ X Y)) (= (CAR (~ X Y)) X))) . NIL . ((CAR #& . 69) (~ #& . 26) (X #& . 29) (Y #& . 34)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 34 .) ((((∀ X U)) (= (CDR (~ X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (~ X U)) U))) . NIL . ((U #& . 1) (X #& . 29) (~ #& . 26) (CDR #& . 71)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 32 .) (4 . |CAR | . UNARY . 950 .) (4 . |CDR | . UNARY . 950 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 72) . (#& . 70) . CDR .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT NIL UNARY 950) . NIL . ((CDR #& . 71) (CAR #& . 69)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 8 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 73) . (#& . 70) . CAR .) ((((∀ X U)) (= (CAR (~ X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (~ X U)) X))) . NIL . ((CAR #& . 69) (~ #& . 26) (X #& . 29) (U #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 30 .) ((((∀ X U)) (¬ (NULL (~ X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (~ X U))))) . NIL . ((U #& . 1) (X #& . 29) (~ #& . 26) (NULL #& . 59)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 28 .) ((((∀ X Y)) (¬ (ATOM (~ X Y)))) . (AXIOM (TM& ((∀ X Y)) (¬ (ATOM (~ X Y))))) . NIL . ((ATOM #& . 61) (~ #& . 26) (X #& . 29) (Y #& . 34)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 26 .) (NIL . (DECL (NNIL) (OT& . GROUND) CONSTANT LISTP) . NIL . ((NNIL #& . 64) (LISTP #& . 10)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 5 .) (CONSTANT . GROUND . LISTP . NIL . NIL . (#& . 65) . NNIL .) (5 . |NULL | . UNARY . 750 .) (5 . |ATOM | . UNARY . 750 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 62) . (#& . 60) . ATOM .) (NIL . (DECL (ATOM NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((NULL #& . 59) (ATOM #& . 61)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 9 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 63) . (#& . 60) . NULL .) ((NULL NNIL) . (AXIOM (TM& NULL NNIL)) . NIL . ((NULL #& . 59) (NNIL #& . 64)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 22 .) (8 . |REVERSE | . UNARY . 950 .) (NIL . (DECL (REVERSE) (OT& (GROUND) . GROUND) CONSTANT NIL UNARY 950) . NIL . ((REVERSE #& . 55)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 74 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 57) . (#& . 56) . REVERSE .) ((((∀ U)) (LISTP (REVERSE U))) . (AXIOM (TM& ((∀ U)) (LISTP (REVERSE U)))) . NIL . ((U #& . 1) (LISTP #& . 23) (REVERSE #& . 55)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 75 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 48) . A1 .) (6 . ALISTP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 52) . (#& . 48) . ALISTP .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 48) . A0 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 48) . A2 .) (NIL . (DECL (ALIST A0 A1 A2) (OT& . GROUND) VARIABLE ALISTP) . NIL . ((A2 #& . 49) (A0 #& . 50) (ALISTP #& . 51) (ALIST #& . 47) (A1 #& . 53)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 64 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 48) . ALIST .) ((((∀ ALIST)) (LISTP ALIST)) . (AXIOM (TM& ((∀ ALIST)) (LISTP ALIST))) . NIL . ((LISTP #& . 23) (ALIST #& . 47)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 65 .) (1 . * . INFIX . 840 .) (NIL . (DECL (*) (FT& ((GROUND GROUND) GROUND NIL . GROUND)) FUNCTIONAL NIL INFIX 840 BOTH) . NIL . NIL . ((* #& . 43)) . NIL . NIL . NIL . LISPAX . NIL . NIL . 55 .) (FUNCTIONAL . (((GROUND GROUND) GROUND NIL . GROUND)) . UNIVERSAL . BOTH . (#& . 45) . (#& . 44) . * .) ((((∀ U V)) (LISTP (* U V))) . (AXIOM (TM& ((∀ U V)) (LISTP (* U V)))) . NIL . ((LISTP #& . 23) (U #& . 1) (V #& . 14)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 56 .) ((((∀ X Y Z)) (LISTP (LIST X Y Z))) . (AXIOM (TM& ((∀ X Y Z)) (LISTP (LIST X Y Z)))) . NIL . ((LISTP #& . 23) (Z #& . 31) (X #& . 29) (Y #& . 34)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 51 .) ((((∀ X Y)) (LISTP (LIST X Y))) . (AXIOM (TM& ((∀ X Y)) (LISTP (LIST X Y)))) . NIL . ((LISTP #& . 23) (X #& . 29) (Y #& . 34)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 47 .) (4 . LIST . PREFIX . 1000 .) (NIL . (DECL (LIST) (FT& ((GROUND) GROUND NIL . GROUND)) FUNCTIONAL) . NIL . NIL . ((LIST #& . 37)) . NIL . NIL . NIL . LISPAX . NIL . NIL . 42 .) (FUNCTIONAL . (((GROUND) GROUND NIL . GROUND)) . UNIVERSAL . NIL . (#& . 39) . (#& . 38) . LIST .) ((((∀ X)) (LISTP (LIST X))) . (AXIOM (TM& ((∀ X)) (LISTP (LIST X)))) . NIL . ((LISTP #& . 23) (X #& . 29)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 43 .) ((((∀ X Y)) (SEXP (~ X Y))) . (AXIOM (TM& ((∀ X Y)) (SEXP (~ X Y)))) . NIL . ((Y #& . 34) (X #& . 29) (~ #& . 26) (SEXP #& . 19)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 24 .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 30) . Y .) (4 . SEXP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 33) . (#& . 30) . SEXP .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 30) . Z .) (NIL . (DECL (X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z #& . 31) (X #& . 29) (SEXP #& . 32) (Y #& . 34)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 2 .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 30) . X .) (1 . ~ . INFIX . 850 .) (NIL . (DECL (~) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL INFIX 850) . NIL . ((~ #& . 26)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 7 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 28) . (#& . 27) . ~ .) (6 . |LISTP | . UNARY . 750 .) (NIL . (DECL (LISTP) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((LISTP #& . 23)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 10 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 25) . (#& . 24) . LISTP .) ((((∀ X U)) (LISTP (~ X U))) . (AXIOM (TM& ((∀ X U)) (LISTP (~ X U)))) . NIL . ((LISTP #& . 23) (~ #& . 26) (X #& . 29) (U #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 14 .) (5 . |SEXP | . UNARY . 750 .) (NIL . (DECL (SEXP) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((SEXP #& . 19)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 11 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 21) . (#& . 20) . SEXP .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . W2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . W0 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V3 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . U2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . U0 .) (5 . LISTP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 11) . (#& . 2) . LISTP .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . U1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . U3 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V0 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . W .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . W1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . W3 .) (NIL . (DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) (OT& . GROUND) VARIABLE LISTP) . NIL . ((W3 #& . 3) (W1 #& . 4) (W #& . 5) (V2 #& . 6) (V0 #& . 7) (U3 #& . 8) (U1 #& . 9) (U #& . 1) (LISTP #& . 10) (U0 #& . 12) (U2 #& . 13) (V #& . 14) (V1 #& . 15) (V3 #& . 16) (W0 #& . 17) (W2 #& . 18)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . U .) ((((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((U #& . 1) (SEXP #& . 19)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 12 .))